Knots as processes: a new kind of invariant

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

y—( Knots as processes: a new kind of invariant

o

L.G. Meredith and David F. Snyder

rf\ Partner, Bio similarity LLC

505 N72nd St, Seattle, WA 98103, USA,
C Igreg. meredith@bio similarity . com

H
O

■i— >

Department of Mathematics
Texas State University — San Marcos
601 University Drive
San Marcos, TX 78666
dsnyder&txstate. edu

ABSTRACT

We exhibit an encoding of knots into processes in the 7r-calculus such that knots are
ambient isotopic if and only their encodings are weakly bisimilar.

^ Keywords: Process calculi, knots, invariants

o

1. Introduction

CN

Knot and link tabulation continues to be a lively area of scientific research and
promises to be useful to areas of science such as quantum computing and DNA
unpacking [22] [32] [H]. The past 20 years have seen major advances in knot clas-
. . sification, the development of knot invariants, and computational methods for tab-

# ^ ulating knots and links. There are tables of the alternating prime knots of up to

23 crossings [25] [5T] [52] [27]. While current algorithms provide complete tables of
knots (and links), winnowing these tables of duplicates is a time consuming task.
Moreover, as knot tables have proved of use to researchers in genetics, and may
prove to be to researchers in quantum computation, the need to search these ta-
bles in meaningful ways presents itself. For example, of the 4,976,016,485 prime,
non-oriented, alternating knots with minimal crossing number of 22, which contain
the tangle corresponding to 5/3 (if any)? Of course, knot invariants are useful to
distinguish knots, but few provide the basis for a formal language of knot properties
with which to identify classes of knots via logical expressions in the language.

1.1. Summary of contributions and outline of paper

Here we present a newly-found strong knot invariant that does give rise to such a
formal language of knot properties. Knots are invariantly associated to expressions
in Milner's 7r-calculus [45], a member of a family of dynamic calculi known as the

1

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

mobile process calculi. These calculi were developed for the analysis of concurrent
computation |46j [56] . The invariant introduced here interprets knot equivalence up
to ambient isotopy as an equivalence of process dynamics known as bisimulation
[59] [57] in the concurrency theory literature. Of critical importance, and somewhat
surprisingly, these two notions of equivalence correspond exactly on the image of
the encoding: the main result of this paper is that two knots are ambient isotopic
if, and only if, their images under the encoding are weakly bisimilar.

Building on this result, we observe that dual to the process calculi are a family
of logics, the Hennessy-Milner logics (HMLs), providing a logical language capable
of the classification of processes via logical properties. Factoring this capability
through our encoding leads to the development of a logical language identifying
classes of knots with logical properties. In particular, the spatial logics discovered by
Caires and Cardelli [9] constitute a particularly interesting sub-family of the HMLs
having logical connectives enabling us to take full advantage of key features of our
encoding. We illustrate the application of the logic in [5] primarily via examples of
predicates that select features of knots.

The paper is organized as follows. First, we provide a brief overview of knot
presentations relevant to this paper, given in the context of the history of knot
tabulation. Next, we give a brief overview of process calculi, highlighting achieve-
ments in that field pertinent to this paper. Section [4] begins the technical exegesis
with an introduction to Milner's polyadic 7r-calculus via demonstration of process
expressions that, much like the combinators of Conway's tangle calculus, reflect
aspects of knot structure (crossings etc.). The section concludes with an example
encoding of the trefoil knot. Section |4.5| gives a condensed but complete formal
presentation of the process calculus. The main theorem is proved in section [5] This
is followed by an account of spatial logic via knots in section [6] and how this can be
applied in the study and inquiry of knot tables, with potential application in knot
tabulation algorithms themselves. Finally, new techniques are judged not solely by
the questions they answer but by the new questions to which they give rise. In the
conclusion, we identify areas of further investigation.

2. A summary of knot presentations

The knot presentations we focus upon herein are the Gauss code [53], the Dowker-
Thistlethwaite (DT) code [17], the Conway notation [15], and the Master Code of
Rankin, Schcrmann and Smith [51] [52j . Other presentation schemes, such as braid
representatives and Morse links, are not directly useful to the development of this
paper and thus are overlooked. We also give a "wish-list" of properties one would
desire from one's knot notation scheme.

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

2.1. Knot presentations

This section briefly discusses various knot notations and establishes some terminol-
ogy, with references for readers needing further details.

2.1.1. Regular knot projections

In 1847, J.B. Listing classified knots up to 5 crossings by analyzing knot projections
[33| . Listing was the first to publish an article containing a drawing of a regular knot
projection (or knot diagram or planar diagram). A knot is taken to be a polygonal
simple closed curve in 3-space. Choose any plane on which projection onto the plane
results in a curve whose only singularities are transverse double points which are
not the image of any vertex from the polygonal curve. Using a canonical normal
vector to the plane for line of sight, for a given double point d we find the point c
in the projection's preimage of d farthest from our line of sight, and we indicate an
undercrossing by erasing the image of a small neighborhood of c from the planar
projection. A careful presentation is given in |37j .

Out of all possible regular projections of a knot, there is (at least) one with
minimal number of crossings.

2.1.2. The Gauss code.

Gauss used regular knot projections to arrive at what is now called the Gauss Code
of a knot 53]. The Gauss code is the first knot notation system. P. G. Tait used
an encoding in the 1870's to classify knots up to 7 crossings [63]. Tait's encoding
may be regarded as an extension to the Gauss Code. One begins somewhere on the
knot projection (not at a crossing point), then proceeds along the knot applying
labels to the first, third, fifth etc. crossing until all crossings are labeled; one then
traverses the knot once more, writing the label of each crossing in the order that
you reach it, attaching a plus or minus sign, depending on whether you are crossing
over or under.

2.1.3. Tait, Little, and Kirkman.

Using Kirkman's classification of certain polygons [3D], Tait (and Little, using sim-
ilar methods) was able to tabulate knots up to 11 crossings [53] [33] [33] [35J. Tait's
system included using a simple reduction rewrite strategy within his notation sys-
tem. This notation was improved by Dowker and Thistlethwaite, as discussed in
some detail below.

2.1.4. Reidemeister moves.

Rcidcmcistcr developed a reduction rewrite system for knot projections (the three
Reidemeister moves) [55]. We illustrate the three moves. The convention in these

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

(and in other graphically-based invariants) is that we show only the relevant part
of the knot. In our diagrams here, we have placed dashed circles, which the reader
should imagine as viewing through scope lens only a portion of the knot, with the
remainder of the knot outside of the scope of view and unchanged.

S> - €

Fig. 1. The three Reidemeister moves. The topmost move will be referred to as Ri, the middle
one as R2, and the bottommost as R3. For any one of these moves R, we write R~^(K) (resp.
R*~(K)) if the move has been applied left-to-right (resp. right-to-left) to the knot diagram K.

The import of this system is Reidemeister's Theorem: an ambient isotopy of
two knots may be exhibited as sequences of rewrites of (any of) their diagrams, and
vice versa. That is, two knots are ambient isotopic if and only if a diagram of one
may be rewritten, via a sequence of Reidemeister moves, to a diagram of the other
[37].

2.1.5. Knotation

Conway developed a clever notational system for tangles, finding an algebraic-like
system for this system that led to several methods of reduction rewrites |15j . He used
this system to retabulate knots and links of 11 crossings by hand, in one afternoon
(an effort that took Tait and Little years of work), discovering one omission and
a few duplications in the process. Conway's system can be used to classify all
arithmetic (also called algebraic, or rational) knots. The Conway code for a knot
originally was given as a basic polyhedron followed by a sorted list of arithmetic
tangles. See Conway's paper [TS] for details. This system has extensions by Caudron
[T4"] and by Bangert [5]. Conway has investigated further structures such as bangles
and bracelets.

2.1.6. Dowker-Thistlethwaite Codes (DT codes)

Dowker created a variation of Tait's notational system that is easier to implement
computationally. Dowker and Thistlethwaite made it the basis for an algorithm

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

that successfully enumerated knots of up to 13 crossings [T7]- Not every DT code
is valid, i.e. an arbitrary DT code may not correspond to an actual knot, and
two distinct composite knots may share the same DT Code. However, a valid DT
code for a prime knot specifies the knot uniquely |61j . In their paper, Dowker and
Thistlethwaite develop an algorithm to filter out invalid cases. They also give a
reduction system to remove duplicates from their enumeration.

We now recall the definition of the DT code of a regular knot projection [17].
Begin at a selected point on the diagram (excepting crossing points) and traverse the
diagram in a selected direction. At each encounter of a crossing, label the crossing
with the next available counting number; for an even label, prepend a negative sign
if traversing the overcross. Returning to the beginning point, each crossing has been
labeled twice, once with an odd number and once with an even number. Let S±
denote the set of labels generated.

If the knot projection has n crossings, then there are 2n labels (from 1 to 2n in
absolute value) and at each crossing an unique odd counting number paired with an
even integer. This induces a parity-reversing function <r on S = {1, . . . , 2n}, where
for each i 6 S we find the crossing with label whose absolute value is i and let
a(i) be the absolute value of the other label at that crossing. Note that a(a(i)) = i
for any i € S. Note that there is also a bijective translation r : S — > S± where
\t(s) \ = s for all s 6 S. Then the DT code of the knot projection is determined by
S = t o a, usually given as the list {S(l), 5(3), . . . , 5(2n — 1)}. Note that 6 o a = t.
Finally, for each i G S, let sgn(i) denote the sign of r(i) (so sgn(i) < implies i is
even) .

For each i 6 S±, let C(i) denote the crossing with label i. Then for any i € S
we know C(i) is adjacent to the two crossings C(i ± 1) and C(8(i) ± 1)), where
addition is modulo 2n. This fact is applied later when giving an explicit algorithm
for encoding a knot.

2.1.7. From Calvo to Rankin, Flint, and Schermann

Calvo developed an inductive knot tabulation algorithm, thereby sidestepping the
need to check validity of DT codes [H] . However, detection of duplication within the
tables generated then becomes the issue. Calvo had the insight that understanding
the deeper flype structure of prime, non-alternating diagram led to greater efficien-
cies in his algorithm. The Calvo algorithm was essentially refined in the development
of a notational system by Rankin, Flint, and Schermann , based on what they call
the group code which reminds one somewhat of the Gauss code but, instead, using
a Conway-likc insertion scheme to allow for easy reduction of flype structures in
the notation [51] [52] [50]. This results in a master array that provides a unique
identifier for prime alternating knots. This forms part of the basis for inductive
construction of all prime alternating knots of crossing size n from those of crossing
size n — l(see the above papers for details). Composite knots remain problematic,
due principally to the issue of detection of duplicates.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

2.2. Desirable properties for a knot presentation system

In this section, we list some properties that one would wish for a knot presenta-
tion system to enjoy, followed by a discussion of the knot presentations of the last
subsection in the light of these wishes.

Due to complexity considerations, one may well despair of a knot notation sys-
tem that would allow for mathematical classification of all knots. However, in de-
signing a system of knot notation or presentation, informed by the history of knot
tabulation and classification we can enumerate the following properties such a no-
tation system may enjoy. These properties invariably correspond to demands of
functoriality on the encoding when considered as a map from the category of knots
or braids to some suitable target category while others are demands on the faith-
fulness (respectively, fullness) of the encoding considered as functor.

• Surjection (realizability) . Each code in the notation represents a knot (or
if this is not the case, those codes that do not represent a knot are easily
recognizable). A code for a knot should be easily obtained from one of its
planar diagrams.

• Reduction. The notation enjoys a calculus with which to reduce and sim-
plify encodings. Each step of simplification or reduction results in an en-
coding representing a knot isotopy equivalent to the originating knot.

• Minimality. The notational encoding of a given knot can be reduced to a
(finite non-empty set of equivalent) minimal encoding(s).

• Well-definedness. If a knot has two (or more) minimal reduced encodings,
each of these encodings is equivalent to the notation for a knot equivalent
via ambient isotopy to the original.

• Injection. Two knots that have equivalent minimal reduced encodings are
ambient isotopic.

• Economy. The notation is computationally cheap and easily constructed
from a diagram of the knot or from a simple code, such as the DT code.

• Compositionality. Operations on knots, e.g. knot composition, correspond
to natural operations on elements in the image of the encoding.

• Separation. The notation can be used to classify a class X of knots, where
X contains a previously classified class of knots (for example, arithmetic
knots (also known as algebraic knots) and bracelets) but is not previously
classified itself.

• Extensibility. The notation enjoys a formal language in which to describe
properties and invariants of notation objects that reflect interesting proper-
ties of knots. This language should also be useful in selecting specific sets of
knots (such as the set of all 21-crossing prime alternating links containing
the tangle 5/3). This language ideally should be scaleable and be applicable
to tables of indefinite size.

The DT code, with proper care taken, satisfies the first six properties but breaks

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

under compositionality. Conway's tangle notation enjoys all of the properties listed,
though the Conway encoding requires foreknowledge of the classes of basic polygons
with n vertices. The master array of Rankin, Flint, and Schermann satisfies the first
five properties, but appears unlikely to support the last four properties to a degree
useful for anything other than tabulation.

2.2.1. A meta-knotation

Due to Reidemeister's Theorem, in order to establish our main theorem we need
only consider diagrams of knots and not knots themselves. Hence we adopt the
following convenient notation and terminology. The meta-variable K ranges over
knot diagrams and we reserve K, to range over knots. For simplicity, we refer to K
as a knot. We write ifc(K) to mean the number of crossing points in the diagram
K but will call this value the crossing number of the knot K, which the reader
is asked not to confuse with the minimal crossing number of the knot (it is in
this sense that we will later say that "two knots from the same isotopy class can
have different crossing numbers"). Formally speaking ~; so will denote equivalence
of knots under ambient isotopy and will denote equivalence of diagrams under
(finite) sequences of Reidemeister transforms. However, when there is little chance
of confusion we drop the subscript and write ~.

3. Concurrent process calculi and spatial logics

In the last thirty years the process calculi have matured into a remarkably power-
ful analytic tool for reasoning about concurrent and distributed systems. Process-
calculus-based algebraical specification of processes began with Milner's Calculus
for Communicating Systems (CCS) [33] and Hoare's Communicating Sequential
Processes (CSP) [23J [7] [35] [53], and continue through the development of the
so-called mobile process calculi, e.g. Milner, Parrow and Walker's 7r-calculus [4"5] .
Cardelli and Caires's spatial logic (TUJ [3] [5J, or Meredith and Radestock's reflective
calculi [3D] [31] . The process-calculus-based algebraical specification of processes has
expanded its scope of applicability to include the specification, analysis, simulation
and execution of processes in domains such as:

• telecommunications, networking, security and application level protocols

n m ED ED;

• programming language semantics and design [35] [5T] [2U] [B"4"] :

• webservices [28] [31] [39] :

• and biological systems [13] [16] [54] [49] .

Among the many reasons for the continued success of this approach are two
central points. First, the process algebras provide a compositional approach to the
specification, analysis and execution of concurrent and distributed systems. Owing
to Milner's original insights into computation as interaction [44], the process calculi

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

are so organized that the behavior — the semantics — of a system may be composed
from the behavior of its components [19] . This means that specifications can be
constructed in terms of components — without a global view of the system — and
assembled into increasingly complete descriptions.

The second central point is that process algebras have a potent proof principle,
yielding a wide range of effective and novel proof techniques [47] [56] [57] [58]. In
particular, bisimulation encapsulates an effective notion of process equivalence that
has been used in applications as far-ranging as algorithmic games semantics [3] and
the construction of model-checkers [8j. The essential notion can be stated in an
intuitively recursive formulation: a bisimulation between two processes P and Q is
an equivalence relation E relating P and Q such that: whatever action of P can be
observed, taking it to a new state P' , can be observed of Q, taking it to a new state
Q' , such that P' is related to Q' by E and vice versa. P and Q are bisimilar if there
is some bisimulation relating them. Part of what makes this notion so robust and
widely applicable is that it is parameterized in the actions observable of processes
P and Q, thus providing a framework for a broad range of equivalences and up-to
techniques [32] all governed by the same core principle [5B] [57] [58] .

4. Knots as processes

This section bootstraps intuitions about the target calculus by introducing process
expressions for key aspects of a knot's structure. An n crossing knot K is modeled as
a system \K\ of concurrently executing processes. More specifically, \K\ is a parallel
composition n" = r 1 [C(z)]|M / of n + 1 processes consisting of n crossing processes
[C(i)J and a process W constituting a "wiring harness." The latter process can
be thought of as the computational equivalent to Conway's "basic polygon," if the
knot is in minimal crossing number form. The complete expression of the encoding
is

IK] := {v ...v 4n ^)(Ilf- x (p u)[C(»)](«4i,...,«4i+3,«)

\n?=oW{v u ^ fi) ,v U ( iA) )\w(v U ( it 2),v U ( it3) ))

Here, C(i) represents the ith crossing in the knot diagram K. The wiring process,
n2r 1 W'(u w (i ) o),«u)(t,i))l^ r ( 1; «(t,2)» t 'w(t,3))) is itself a parallel composition of wire pro-
cesses that correspond to edges in the 4-valent graph of the knot shadow [61] the
constraints of which are reflected in the indexing function u>. The wiring process
may be calculated from other knot notations. For example, we later show how the
indexing function uj may be calculated from S, the DT code of the knot projection.
The crossing and wire processes have further substructure, outlined below.

Remark 4.1 (knots as abstractions). The reader familiar with process calculi
will observe that the encoding actually produces an abstraction [56 in A^j={K)
names (see the first choice in the production labeled agent in the grammar of |4.5[).

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

This is actually a way of demarking that the encoding should be insensitive to the
particular set of names chosen to represent the ports of the crossings. Some caution
must be exercised, however, as the encoding only preserves knot structure if the
abstraction is applied to a vector of A#(K) distinct names.

4.1. Crossing processes

A crossing is conceived in the diagram below as a black-box having four points of
external interaction (ports) with the remainder of the knot process and as having
two internal wires each connecting a pair of ports. As a process, the crossing has
four possible behaviors, as shown in the defining encoding below.

yo yr

Fig. 2. Crossing process

C(x ,x 1 ,y Q ,y 1 ,u) <- x 1 ?(s).y l(s).(C(x ,x 1 ,y ,y 1 ,u)\ul)
+yo?(s).x 1 l(s).(C(x ,x 1 ,y ,y 1 ,u)\ul)
+xo?(s).(C'(x , X!,y , yi, it, yi))
+y 1 1(s).(C'(x , xi, y , Vi,u, x ))

where

C"(x , xi, y , yi,u, v) «- xi?(s).y \(s).(C'{x Q , Xi,y , yi,u, v)\u\)
+y ?(s).x 1 l(s).(C'(x ,x 1 ,yo,yi,u,v)\ul)
+u7.vl(s).(C(x a ,x 1 ,yo,y 1 ,u))

A crossing process has four ports xq , x\ , t/o , 2/1 and a hidden synchronizer u.
Each port has a partner port, linked as shown in the diagram (note the relationship
to Conway's ±1 tangles [H>|). For example, the first behavior (indicated by the first
term of the summand) is that the process listens at port xi for a signal s (which
will come, if at all, via the wiring process). Having heard s, the signal is passed
directly to the port yo where the signal is then broadcast via the wiring process.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Then the process alerts the hidden synchronizer u that a signal has been passed
between the ports, while concurrently preparing itself for further signal processing.
The second summand represents a signal passing along the same strand in the
opposite direction. The third and fourth summands are similar to the first two,
except that before passing any received signal to its partner port, the process waits
for a signal from the synchronizer u before allowing the signal to pass, while still
allowing a signal to pass between x\ and yo if the synchronizer has not yet been
alerted. So the role of u is that of a traffic controller who gives priority to traffic
over the route between x\ and yo, mimicking an over-crossing.

4.2. Wirings

As an illustration of the expressive power of the formalism, taken together with the
short description of the process calculus in the next section, the definitions below
fully equip the interested reader to verify that wire processes are lossless, infinite
capacity buffers.

W(x,y) <— [y n m)(Waiting(x,n,rn)\Waiting(y,m,n))
Waiting(x,c,n) <— xl{v).{i> m)(Cell(n,v,m)\Waiting(x,c 7 m))

+c?(w).c?(c).Ready(x, c, n, w)
Ready{x 1 c, n, w) 4— xl{v).(v m)(Cell(n, v, m)\Ready(x, c, m, w j)
+xl(w).Waiting(x, c, n)
Cell(c,v,n) 4- c!(w).c!(n).0

The ports x and y in which W is parameterized may be intuitively considered
splice points in the knot diagram. We adopt this terminology in the sequel.

One may well wonder why perfect buffers are chosen to represent wires. For
example, the following process intuitively captures a notion of wire.

Relay(x, y) := x?(s).yl(s). Relay <{x, y) + yl(s).x\(s).Relay(x, y)

The problem is one of composition. Foreshadowing the method of proof, in the
sequel we will need to compose wires and crossings and have the result act as a
wire. For example, if W(x, y) represents a candidate for wire behavior, to model
the first Rcidemeister move we have a demand that

W{y ,yi) ~ {v x xi w w 1 )(W(y , w )\(v u)C(x ,xi,w ,wi,u)\W(x ,xi)\W(yi,w 1 ))

Again, the reader may verify that while this is true of buffers, it is not true of
the Relay process defined above.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

4.3. An example: the trefoil knot as a process

The above intuitions are illustrated with an example, showing one way to represent
the trefoil knot as a process. Following the schema above, the process encoding of the
trefoil knot is a parallel composition of three crossing circuits with a wiring harness
whose design ensures that the crossing circuits are connected to each other in a
way that respects the knot diagram. Additionally, we make each synchronization
channel local to each crossing via a restriction on that channel.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

[3i] = (v ...v 5 )(v u )C(vo 7 v 1 ,v 2 ,v 3 ,u )
\W(v 2 ,v 7 )\W(v 3 ,v 6 )
\{v ui)C(v 4 ,v 5 ,v e ,v 7 ,ui)
\W(v 4 ,v 9 )\W(v 5 ,v 8 )

\(U U2)C(V8,VQ,V W ,VU,U 2 )

\W(v w , v )\W(vu,vi)

4.4. The distinguishing power of dynamics

In summary, to each knot K, the encoding associates an invariant \K\ , an expression
in a calculus of message-passing processes via an encoding of a diagram of the knot.
More precisely, given the set of knot diagrams K and the set of processes modulo

structural equivalence P (see section 4.5 ), the encoding induces a map, [— ] : K — >• P.
Most importantly, the notion of equivalence of knots coincides perfectly with the
notion of equivalence of processes, i.e. bisimulation (written here and in the sequel
~). Stated more formally,

Theorem 4.2 (main).

Ki~K* ^ ~ [#- 2 ].

In particular, in contrast to other invariants, the alignment of process dynamics
with knot characteristics is what enables the invariant identified here to be perfectly
distinguishing. As discussed below, among the other beneficial consequences of this
alignment is the ability to apply process logics, especially the spatial sub-family of
the Hennessy-Milner logics, to reason about knot characteristics and knot classes.

We see moreover the possibility of a deeper connection. As mentioned in the
previous section, bisimulation has turned out to a powerful proof technique in the
theory of computation adaptable to a wide range of situations and admitting a
number of potent up-to techniques [59] . One of the central aims of this research is
to broaden the domain of applicability of bisimulation-based proof methods.

4.5. The syntax and semantics of the notation system

Having bootstrapped an intuitive account of the target calculus via the encoding,
we now summarize a technical presentation of this calculus. The typical presenta-
tion of such a calculus follows the style of giving generators and relations on them.
The grammar, below, describing term constructors, freely generates the set of pro-
cesses, V. This set is then quotiented by a relation known as structural congruence,
yielding the set P mentioned above in the type signature of the map constituting
the encoding.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

4.5.1. Process grammar

SUMMATION AGENT

M,N::=0 \ x.A \M + N A ::= (x)P \ [x]P

PROCESS

P, Q::=N\ P\Q \X(y) | (rec X{x).P){y) \ (v x)P

Note that x denotes a vector of names of length \x\. In the encodings for knots,
crossings and wires given above we adopted the following standard abbreviations.

xl{y).P:=x.{y)P x\(y).P := x.[y\P X(y) <- P := (y)(rec X($).P)(y)

U^P i :=P Q \...\P n . 1

4.5.2. Structural congruence

Free and bound names and alpha-equivalence. At the core of structural
equivalence is alpha-equivalence which identifies process that are the same up to a
change of variable. Formally, we recognize the distinction between free and bound
names. The free names of a process, J-M(P), may be calculated recursively as
follows:

J7V(0) :=

TM{x7{y).P) := {x}U (TAf(P)\{y}) TAf(x!(y).P) := {x} U {y} U FM{P)
TN{P\Q) := TN{P) U FN{Q) TN{P + Q) := TN{P) U FN{Q)
FN{{v y)P) := FN{P) \ {y}
J-AA((rec X(x).P)(y)) := {y} U FN{P) \ {x}

The bound names of a process, BJV(P), are those names occurring in P that
are not free. For example, in x7(y).0, the name x is free, while y is bound.

Definition 4.3. Then two processes, P,Q, are alpha-equivalent if P = Q{y/x}
for some x G BN{Q),y G BAf(P), where Q{y/x} denotes the capture-avoiding
substitution of y for x in Q.

Definition 4.4. The structural congruence [56j , =, between processes is the least
congruence containing alpha-equivalence, satisfying the abelian monoid laws (as-
sociativity, commutativity and as identity) for parallel composition | and for

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

summation +, in addition to the following axioms:

(vx)0 = (v x){v x)P = {v x)P (u x){v y)P = (v y)(u x)P

P\(v x)Q = {v x)(P\Q), if xg FN{P)

(rec X(x).P)(y) = P{y/x}{(rec X(x).P)/X}

4.5.3. Operational semantics

Finally, we introduce the computational dynamics. What marks these algebras
as distinct from other more traditionally studied algebraic structures, e.g. vector
spaces or polynomial rings, is the manner in which dynamics is captured. In tradi-
tional structures, dynamics is typically expressed through morphisms between such
structures, as in linear maps between vector spaces or morphisms between rings. In
algebras associated with the semantics of computation, the dynamics is expressed
as part of the algebraic structure itself, through a reduction reduction relation typ-
ically denoted by — >. Below, we give a recursive presentation of this relation for the
calculus used in the encoding.

COMM

yC\v = % \v\ = \A

x.{y)P I x.(uv)[z\P^ {vv){P{z/y}\Q)

Par Equiv New

P -> P' P = P' P' -+Q' Q' = Q P -> P'

P\Q->P'\Q P^Q (vx)P^(vx)P'

We write =>■ for ->*, and P — > if 3Q such that P — > Q.

In closing this summary, we take the opportunity to observe that it is precisely
the dynamics that distinguishes this encoding. The equivalence that coincides with
knot equivalence is a behavioral equivalence, i.e. an equivalence of the dynamics of
processes in the image of the encoding. In a marked departure from Gauss codes or
DT codes or Conway's "knotation," this facet of the encoding affords the conflation
of notation scheme with invariant, providing a framework in which to establish the
distinguishing power of the invariant and a language in which to express classes of
knots as logical properties, as discussed in subsection [6]

4.5.4. Bisimulation

The computational dynamics gives rise to another kind of equivalence, the equiva-
lence of computational behavior. As previously mentioned this is typically captured
via some form of bisimulation.

The notion we use in this paper is derived from weak barbed bisimulation [45] .
We must introduce an "up to" (60] [48] strategy to deal with the fact that Rei-

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

demeister moves can not only introduce or eliminate crossings (see R\ R2), but
"reorder" them (see R3).

Definition 4.5. An agent B occurs unguarded in A if it has an occurence in A not
guarded by a prefix x. A process P is observable at x, written here P \. x, if some
agent x.A occurs unguarded in P. We write P JJ. x if there is Q such that P =>■ Q
and Q I x.

Definition 4.6. A barbed bisimulation is a symmetric binary relation S between
agents such that P S Q implies:

(1) If P -> P' then Q^Q' and P' S Q' , for some Q' .

(2) If P I z, then Q |L x.

P is barbed bisimilar to Q, written P ~ Q, if P 5 Q for a barbed bisimulation 5.

4.5.5. Contexts

One of the principle advantages of computational calculi like the 7r-calculus is a
well-defined notion of context, contextual-equivalence and a correlation between
contextual-equivalence and notions of bisimulation. The notion of context allows
the decomposition of a process into (sub-)process and its syntactic environment, its
context. Thus, a context may be thought of as a process with a "hole" (written □)
in it. The application of a context M to a process P, written M[P], is tantamount
to filling the hole in M with P. In this paper we do not need the full weight of this
theory but do make use of the notion of context in the proof the main theorem. As
will be seen, the Reidmeister moves amount to decomposing the representation of
the knot into some collection of crossings or wires and the rest of the knot.

SUMMATION AGENT

M Ml M N ::= □ | x.M A | M M + M N M A ::= (x)M P | [x\M P

PROCESS

M P ::= M N \ P\M P |(rec X(x).M P ){y) \ (u x)M P

Definition 4.7 (contextual application). Given a context M, and process P,
we define the contextual application, M[P] := M{PjO}. That is, the contextual
application of M to P is the substitution of P for □ in M.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Example 4.8. For example, if we take

M 3l := (v ...v 5 )(u u Q )C(v , vi,v 2 ,v 3 , u )
\W(v 2 ,v 7 )\D

\{v Ui)C(v 4 ,V 5 ,V 6 ,V 7 ,Ui)

\W(v i7 Vg)\W(v 5 ,V 8 )

\{v U 2 )C(V8,Vg,Vi ,Vu,U 2 )

\W(v w , '^o)|W / («ii,wi)

then l3 1 }=M 3l [W(v 3 ,v 6 )}

5. Main theorem: proof sketch

We have a couple of technicalities to dispatch. To motivate the first of these we wish
to note that the arguments for the forward direction require some care. The aim is
to capture the intuitive equivalence-preserving nature of the Reidemeister moves as
corresponding bisimularity-preserving transformations on processes (in the image
of the encoding) . Because of the encoding of crossing information of wires in terms
of synchronization of signal-flow, we have to introduce "enough signal" to keep the
knot "firing" , as it were, to establish that the process transformations corresponding
to the knot transformations are bisimulation-preserving. Rather than seeing this
extra condition as a weakness of the approach we submit that this feature provides
evidence to our claim that the characterization of ambient isotopy of knots at work
in this encoding is in terms of process dynamics.

We will say that the encoding of a knot is alive as long as it is firing, i.e. the
process is enabled to make a reduction step. If it ever ceases to push signal through,
i.e. process cannot make a reduction step, then it is dead.

We can ascertain an upperbound on initial signal that guarantees liveness of
the encoding. Surely, the parallel composition of 2#(if) barbs, i.e. two barbs for
each crossing, will guarantee the liveness of the encoding. More declaratively, we
simply demand that [K] \init Signal be live before we are willing to admit it as a
representation of the knot.

Definition 5.1. More precisely, we will call the pair ([if], initSignal) alive
if initSignal is an abstraction over a parallel composition of barbs, with
\initSignal\ = we demand that for any vector of distinct names, v with

M = 1 1-^1 1 an d any state, K' , such that \K\{v)\initSignal{v) => K' we have that

Different crossing numbers mean different numbers of free names. Knots
in the same isotopy class may have diagrams with different numbers of crossings.
Different numbers of crossings lead to different aritics in the abstractions, so in
interpreting these knots we haveto work to properly capture the notion of equiva-

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

lence. While the precise statement is somewhat technical, the intuition is simple: it
is possible to find a common "interface" , i.e. argument list, between the two knots
such that restricting to that argument list obtains bisimilar processes.

Imagine (the processes that interpret) knots as programs housed in boxes with
ports on the perimeter. Two knot diagrams Ki,i e {1,2}, from the same isotopy
class may have different crossing numbers and thus their boxes have different num-
bers #(Ki) of ports on the outside. We can find a number of ports, call it n,
somewhere between the minimal crossing number of the isotopy class and the lesser
of #{Ki) such that if - using restriction - we close off #(K\) — n ports on the
first box and #(K 2 ) — n on the second we get two boxes that perform the same
observable set of signal processing steps.

Formally, suppose K\ ~ K 2 and let #Min(K) '■= min{#(K') : K' ~ K}. We
assert that there is an n such that 4# Mi „(if 1 ) < n < 4 * min{#(Ki), #(K 2 )} and
for any vector of names, v, with \v\ = n and v[i] 7^ v[j] •<=>■ i ^ j, there exists
two vectors of names, Wi,w 2 , also all distinct, such that

(y w^lK.Kv : w,) ~ {u w 2 )[K 2 \{v : w 2 )

with I toil = 4#(if l ) - n.

Prime versus composite knots. Finally, we need to say a little about how we ob-
tain a 7r-calculus expression for a given knot diagram. We use another bootstrapping
procedure, beginning with another knot notation (Dowker-Thistlethwaite codes is
used here) and exhibiting an algorithm for calculating a process expression from
the chosen notation scheme. The reader will note that DT codes are unique only
when restricted to the class of prime knots. It turns out that our encoding preserves
knot composition. In fact, knot composition turns out to be a specialized form of a
procedure, parallel composition + hiding, long-investigated in the process-algebraic
setting. So, it is sufficient to demonstrate the encoding for prime knots.

5.1. Forward direction. K x ~ K 2 =>- [-Ki] — [-K2]

Strategy and intuitions. Since K\ ~ K 2 we know there is a sequence of Rei-
demeister moves converting K\ to K 2 . Each move is proved to correspond to a
bisimilarity-preserving transformation on a related process. We establish context
and substitution lemmas and as a consequence obtain that the process operations
corresponding to the Reidemeister moves preserve bisimularity. As noted above, a
small amount of bookkeeping is required to iteratively apply these transformations
to mirror Reidemeister moves as applied in a proof of ambient isotopy of two knots.

We begin by observing that the intuition behind the Reidmeister moves is funda-
mentally about performing local operations, i.e. on some subset of wires or crossings,
while leaving the rest of the process unchanged. We interpret this notion of a "local
operation" , say R, on a knot diagram K schematically as follows.

• factor the process, \K\, as M[njCj|iTjWj] where niCi|IL;Wi encodes the set

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Fig. 4. The figure illustrates a Reidemeister move of the first type as reflected in the context M
of the 3i knot, as given in Ex. |4.8|

of crossings or wires to be modified by R, i.e. the left side of the move to be
performed, and M is the context representing the unchanged portion of the
process;

• letting R~^(K) (resp. R^(K)) denote the left-to-right (resp. right-to-left) ap-
plication of the move R to K, then [R - *'^)] is calculated as M[n.j/(7|, |ILy/Wj-'],
where HiiC' v \HjiWji are the processes interpreting the modified set of crossings
or wires, i.e. the right side of the move to be performed.

The mathematical content of these statements is that the encoding naturally
extends to an encoding {Ri{L, R}J of the left and right hand sides of each Reidemeis-
ter move such that {Kj = M[[R;Z]] (resp. M[[i?;R]]) and {Ri*(K)j = M[[R;R]]
(resp. [R^~(-Fl)] = M[[RjX]]). Here, a picture really is worth a thousand words (see
figure [5]) .

478] taking M 3l
3i

to
to

be the encoding
the strand corre-

Example 5.2. For example, as in
of Ri(3t,W(v3,ve)), the application of Ri to 3i at
sponding to the wire process W(v 3 ,vq) is given by [Ri(3i, W(vs, v 6 ))j =
[v x x\ y 2/i)M 3l [((v u)C(xo,x 1 ,yo,y 1 ,u)\W(xo,x 1 )\W{yo,v 3 )\W(y 1 ,v 6 ))}. See
figure |4]

A certain discipline is required in the extended encoding. To establish our sub-
stitution and context lemmas we have to keep the interface (i.e. the ports in the
process expression corresponding to the splice points) of the left and right hand
sides of the R-move the same. So, for R\L and R2L we must restrict the ports that
are not the splice points. One way to address this is to embed the restrictions into
the encodings of R\L and R2L. Algebraically,

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Fig. 5. Reidemeister moves as bisimilarity-preserving transformations. Cf. Fig.^

[i? 1 L](yO,yl) =

(y x xi w Wi)(W(y , w )

\(p u)C(x ,xi,wo,wi,u)\W(x ,xi)

\W( yi ,wi))

[i? 2 i](a;oo,a;oi,^io,^ii) =
(y Voo, Voi, 2/io, t/ii, w 00 , tuoijtoio, u>ii)(W(xoo, u>oo)\W(xoi, t«oi)

\(v u )C(wqo,w 01 , 2/00, 2/oi, wO)

\W(y o,yu)\W(yoi,yio)

\(v ui)C(wi , wn, 2/10, 2/n, wi)

|W A (a;io,'u;io)|VF(a;ii,wii))

Keeping to the notion of equivalence outlined in the section above, however, it
will be convenient to factor out the restrictions as in the example above.

Lemma 5.3 (context). Vi € {1,2,3} if K\ ^ i^en //iere exists a context M

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

and (possibly empty) vector of distinct names w such that

(y w)\K x \{v^w) = {vw)M\\R l L\\
\K 2 \ = M{lR t R]}

Proof. This follows directly from the definition of the encoding. □

Lemma 5.4 (substitution). For all i e {1,2,3} RiL is bisimilar to RiR in the
context of a live encoding. That is, if

• \K\\initSignal is alive, and

• {K\\initSignal = M[[i?,L]]

for some context M then we can substitute [RiR] in its place without change of
behavior, i.e.

(vw)M[[RiL}] ~ M[lR t Rj] , Vi e {1,2,3}

Proof. This follows from the definitions of \Ri{L, R}j plus the requirement that
M derives from a live encoding. Even if one side has additional synchronizations,
there is always enough signal to overcome spurious blocking. □

An immediate consequence of these two lemmas is

Lemma 5.5 (1-step). if K\ can be derived from K 2 by application of one Reide-
meister move, then

[JfiKw) ~ (i/ w)\K 2 \(v:w)

We are almost in a position to complete the proof of the forward implication.
The next step is to show that you can iterate the performance of these bisimilarity-
preserving transformations in a way that precisely mimics iterated application of
Reidemeister moves. Because the moves R\ and R 2 change the number of crossings
the number of ports in the interface of the (encoding of the) knot to which they
are applied changes. This is the core issue in the formal statement of the theorem.
Because the splice interface remains constant across the two sides of a Reidemeister
move all one has to do is keep track of the ports to be hidden. The complete proof
uses a case analysis of the composition of any two types of Reidemeister moves.
We illustrate the analysis in the case of a simplifying (crossing-elimination) R\ step
followed by a complicating (crossing-introducing) R 2 step.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

• The R\L — > R\R step means we have a context M such that

{v x xi w Wi)[Xi](wo : x : x x : w : wi)

= (y xo x l wo w^MllRrL}}
~ MgR.Rj]
= lK 2 j(vo).

• The R2R — > R2L step means we have a context M' such that

(u yoo ■■ ■ yn w Q0 ... wxi)lK a }{vi : y 00 : . . . : yn

woo ■ ■ ■ ■ ■ wii)
w n )M'[lR 2 L]\

= Voo ■ ■ ■ Vxx woo ■ ■
~ M'WR.R}]

- [Km).

• Since Vq,v{ are just lists of distinct names with \v^\ = Ip^JI = just pick
Vq = v\. Dropping the subscript, we conclude

[y xo x 1 w w^lKxjiv : x : x x : w ■ Wi) ~
(v yoo--- yn w 00 --- wn)[X 3 ](ul : y 00 : . . . : yn : w o ■ ■ ■ ■ ■ %)

• Moreover, we have [-K2](i5) forming the shared core.

The attentive reader might wonder how R3 works. Indeed, Perko pairs provide
a key counter example to using restriction. This is where bisimulation really shows
it's value - in the form of its flexibility. The outline follows the proof technique of
bisimulation- up-to (in this case, up to context), found in |57j after noting that that
there are two simple paths in the knot encoding between any given pair of distinct
ports.

5.2. Reverse direction. K 1 ~ K 2 -t= [[i^i] ~ [[K2]

We prove this by contradiction, assuming two knots in distinct isotopy classes with
bisimilar images and arriving at absurdity. Not surprisingly, the argument in this
direction is considerably less complicated as it is nonconstructive.

Without loss of generality (by application of the lemmas of the forward direction
as needed), we assume knots are given in minimal crossing diagrams. Due to this
minimality, if the crossing numbers of these diagrams are different, then the number
of free names (or arity of the abstractions interpreting the knots) in [ifi] differs
from those in [-K2] -contradicting bisimilarity. Thus, the crossing numbers must be
the same.

Now we employ the form of the encoding: n'/Z 1 [C'(i)](...)|n™ ; r 1 W^(...)|W / (...) ~
n"r 1 [C , (j)](...)|n™r 1 l^ / (...)|W // (...). Notice that a consequence of sharing the same
crossing number is that the crossing process part of the two encodings is iden-
tical. Because bisimulation is a congruence this implies H^- 1 W(...)\W{...) ~

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

WJ~qW' (...)\W (...). This says that the only difference can be in the "wiring har-
nesses". Obviously, if any of these wires differ (up to a-equivalence), then there is
a distinguishing barb, contradicting our assumption of bisimulation. Hence none of
the wires differ, their respective sets of crossings are wired identically, which means
the diagrams are identical. Thus, the knots are ambiently isotopic - a contradiction.

6. Unlikely characters: spatial logic for knots

Associated to the mobile process calculi are a family of logics known as the
Hennessy-Milner logics. These logics typically enjoy a semantics interpreting for-
mulae as sets of processes that when factored through the encoding outlined above
allows an identification of classes of knots with logical formulae. In the context of
this encoding the sub-family known as the spatial logics [3] [10] [E] are of particular
interest providing several important features for expressing and reasoning about
properties (i.e. classes) of knots. We hint here at how this may be done.

6.0.1. Structural connectives

The spatial logics enjoy structural connectives corresponding, at the logical level, to
the parallel composition (P\Q) and new name {(v x)P) connectives for processes.
As illustrated in the examples below, these connectives are extremely expressive
given the shape of our encoding.

6.0.2. Decideable satisfaction

In [5] the satisfaction relation is shown to be decideable for a rich class of processes.
It further turns out that the image of the our encoding is a proper subset of that
class. This result provides the basis for an algorithm by which to search for knots
enjoying a given property.

6.0.3. Characteristic formulae

In the same paper [5] , Caires presents a means of calculating characteristic formu-
lae, selecting equivalence classes of processes up to a pre-specified depth limit on
the support set of names. Composed with our encoding, this characteristic formula
can be used to select characteristic formulae for knots.

6.0.4. Spatial logic formulae

The grammar below (segmented for comprehension) summarizes the syntax of spa-
tial logic formulae. We employ illustrative examples in the sequel to provide an
intuitive understanding of their meaning referring the reader to [8] for a more de-
tailed explication of the semantics.

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

BOOLEAN SPATIAL

A, B ::=T \ ->A \ A A B \ rj = rj' | | A\B \ x®A | Vx.A | Hx.A

BEHAVIORAL RECURSION ACTION NAME

| a.A | X{u) | tiX{u).A a (x?(y)) \ (xl(y)) | (r) n ::= x | r

6.1. Example formulae
6.1.1. Crossing as formula.

{j,C{x , Xi,y , y 1 ,u).{(x ?(z))((ul)(y 1 lz)C(x , xx, yo,yi,u))
A (yi^(z))((ul)(x lz)C(x Q , x-l, 2/0,2/1, «))
A (xi?(z))((u?) (y lz)C(x , xi,y , y\,u))
A (yo?(^))((w?)(2:i!z)C(:Eo,2i,?/o,yi,w)))

The lexicographical similarity between the shape of this formulae and the shape
of definition of the process representing a crossing reveals the intuitive meaning of
this formulae. It describes the capabilities of a process that has the right to represent
a crossing. For example it picks out processes that may perform an input on the
port xq in its initial menu of capabilities. What differentiates the formula from the
process, however, is that the crossing process is the smallest candidate to satisfy the
formula. Infinitely many other processes - with internal behavior hidden behind this
interface, so to speak - also satisfy this formula. Even this simple formula, then, can
be seen to open a new view onto knots, providing a computational interpretation
of virtual knots.

Note that this formula is derived by hand. A similar formula can be derived
by employing Caires' calculation of characteristic formula [8] to the process repre-
senting a crossing. In light of this discussion, we let [CJ^xO, xl, yO, yl, u) denote
a formula specifying the dynamics we wish to capture of a crossing. To guaran-
tee we preserve the shape of the interface and minimal semantics we demand that
[CJ^xO, xl, j/0, yl, u) C(a;0, xl, 2/0, yl, u) where C{xQ, xl, yO, yl, u) denotes the
formula above.

6.1.2. Crossing number constraints.

The moral content of the context lemma (Lemma 5.3) is that the notion of "local-
ity" in the Reidemeister moves is effectively captured by the parallel composition
operator of the process calculus. This intuition extends through the logic. Given
a formula, [CJ^xO, xl, yO, yl, u), we can use the structural connectives to specify

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

constraints on crossing numbers, such as at least n crossings, or exactly n crossings.

AT-LEAST-N

K f n (xs,ys) := U^Hu.lCfl^(xsi,ysi,u)\T

EXACTLY- N

K $ n (xs, ys) := II "Zq 1 Hu.lCl$(xsi,ysi,u)\-i (Vx , y , x\ , y 1 , u. [C] ^ (x , Vo , xi , Vi , u) \ T)

To round out this section, recall that the encoding of an n-crossing knot decom-
poses into a parallel composition of n copies of a crossing process together with
a wiring harness. To specify different knot classes with the same crossing number
amounts to specifying logical constraints on the wiring harness. In the interest of
space, we defer examples to a forthcoming paper. Suffice it to say that both the
conditions "alternating knot" and "contains the tangle corresponding to 5/3" are
expressible. For example, it is possible to calculate the characteristic formula of a
process corresponding to the tangle 5/3 and conjoin it into the classifying formula
via the composition connective of the logic.

Finally, we wish to observe that it is entirely within reason to contemplate a
more domain-specific version of spatial logic tailored to the shape of processes in
the image of the encoding. Such a domain-specific logic would have a better claim
to the title formal language of knot properties.

7. Conclusions and future work
7.1. Knotation system properties

Rather than list the properties of section |2.2| and tick them off, as we may do, let
us take a step back. In the end it is the act of calculating over knots - tabulat-
ing, searching, making new ones from old - that places demands on the notation
system used to represent them. These are the practical considerations that give
rise to the properties listed in |2.2| Establishing the tight correspondence between
processes in the image of the encoding and the knots they represent is ultimately
in service of showing this is a reasonable proxy for knots because calculations on
the representation have a correspondence to calculations on the domain. Moreover,
the last few decades of logic in computer science has taught us that there is fidelity
and then there is fidelity. It's one thing map elements of one domain to elements of
another, but it's another to map the procedures of one domain (roughly, operations
on elements) to the procedures of another. Whether one sees a demand like this
through the lens of "functoriality" or through a correspondence of proofs (of say,
ambient isotopy, in a proof system made of Reidmeister moves) and programs (that
transform programs) , the practical side of the demand is about making calculation
tractable, so that "local" operations in one domain correspond to "local" opera-
tions in the other. This makes it possible to structure calculations in terms of the
structure of the elements over which the calculations are being performed, which
has far-ranging consequences on the complexity of calculation in the representative

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

domain. Of note, we have been careful to restrict attention to the image of the
encoding. We do not, as of yet, have an effective characterization of processes that
will decide whether or not a process is in the image of the encoding. This restriction
notwithstanding, the image is the only system thus far proposed that does enjoy
all of the properties listed, including possessing (actually, being) a language for
classifying knots via logical properties.

7.2. Knot queries

The interest in knot tabulation coming from the physical sciences is a strong mo-
tivation to investigate the design of a specialized form of spatial logic tailored to
reasoning about processes in the image of this encoding. Specifically, the current
authors are in the process of devising an executable knot query language that runs
on top of a translation of spatial logic predicates to XQuery, the XML query lan-
guage [?] [55]. In this application, a member, K, of an isotopy class [K]~ is stored
as an XML document [[if]]xML- As the notation indicates, the document may
be calculated from the process expression, {KJ. Pleasantly, all such documents will
conform to an XML schema [I5J [55J that may be formally derived from the

grammar for processes described in section 4.5.1 Thus, the mathematics extends
to a formal specification of the software implementation of a "knot database" and
the compositional nature of the specification makes tractable formal verification of
the correctness of the software with regards to the specification.

7.3. Braids, tangles, virtual knots, racks and quandles

As may be seen from the encoding of the Reidcmcister moves, nothing in this
approach restricts it to knots. In particular, the same techniques may be lifted to
braids and tangles. More generally, Kauffman posits an intriguing new member to
the knot family by virtualizing the crossings in a knot diagram |29j . We note that
while we arrived at this encoding before becoming aware of Kauffman's work, that
line of investigation is very much aligned to the guiding intuitions of the encoding
presented here. Namely, the crossing circuit a priori could be any 7r-calculus process
that respects the interface of the wiring circuit. We conjecture that many forms of
virtualization may be faithfully interpreted as simulation.

Moreover, it seems likely that the rack and quandle frameworks may be mirrored
in the process calculus, as these structures can be used to model the action of the
Reidemeister moves on a knot. The relation between this type of action and the
dynamics of the process calculus presented here remains to be investigated.

7.4. Other calculi, other bisimulations and geometry as behavior

The astute reader may have noticed that the encoding described here is not much
more than a linear notation for a minimal graph-based representation of a knot di-
agram. In this sense, there appears to be nothing particularly remarkable about the

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

representation. Though expressed in a seemingly idiosyncratic way, the encoding is
built from the same information that any freely downloadable program for calculat-
ing knot polynomials uses routinely. What is remarkable about this representational
framework is that it enjoys an independent interpretation as the description of the
behavior of concurrently executing processes. Moreover, the notion of the equiv-
alence of the behavior of two processes (in the image of the encoding) coincides
exactly with the notion of knot equivalence. It is the precise alignment of indepen-
dently discovered notions that often indicates a phenomena worth investigating.

This line of thought seems particularly strengthened when we recall the ir-
calculus is just one of many 'computational calculi' — the A-calculus being an-
other paradigmatic example — that may be thought of as a computational dynam-
ics+algebra and that virtually every such calculus is susceptible to a wide range of
bisimulation and bisimulation up-to techniques |42j . As such, we see the invariant
discussed here as one of many potential such invariants drawn from these relatively
new algebraic structures. It is in this sense that we see it as a new kind of invariant
and is the inspiration for the other half of the title of this paper.

Finally, if the reader will permit a brief moment of philosophical reflection, we
conclude by observing that such a connection fits into a wider historical context.
There is a long-standing enquiry and debate into the nature of physical space.
Using the now familiar signposts, Newton's physics — which sees space as an ab-
solute framework — and Einstein's — which sees it as arising from and shaping
interaction — we see this connection as fitting squarely within the Einsteinian
Weltanschauung. On the other hand, unlike the particular mathematical framework
of continuity in which Einstein worked out his programme, behavior and its implied
notions of space and time are entirely discrete in this setting, built out of names
and acts of communication. In this light we look forward to revisiting the now well-
established connection between the various knot invariants such as the Kauffman
bracket and quantum groups. Specifically, it appears that the kinematic picture of
loop quantum gravity derived from spin networks can be faithfully encoded in a
manner analogous to one used here to encode knots, but the process structure offers
an account of dynamics somewhat different from spin foams [4] .

8. Appendix: From DT-codes to processes

What follows is an algorithm for calculating the u indexing function. Note that the
function over can be implemented easily using the function 5, or the function sgn,
described in section 2.1.6 Exercise for the reader: upgrade the algorithm so that
wires are not duplicated during the process.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

* *)

* *)

* Given types Knot and Wire, the omega function is typed as follows *)

* omega : int -> (int -> int) -> (int -> int) -> Knot -> (Wire list) *)

* With dt a table representing the Dowker-Thistlethwaite mapping *)

* from odds to evens, and dti the inverse. The function keeps an *)

* accumulator, acc, in which to collect the wires it calculates. *)

* The function assumes helper functions C and x0,xl,y0,yl. C takes *)

* and instance of type Knot and the odd index of the DT code and *)

* returns the crossing. The other helpers are accessors of the ports *)

* of the crossing. The algorithm visits every crossing and so *)

* generates many wires more than once, which is why the accumulator *)

* is updated with union rather than cons on the recursive calls. As *)

* an exercise, modify the algorithm to avoid wire duplication. *)

* *)
* *)

let omega i dt dti knot acc =
if (i <= (numCrossings knot))
then

let ic = (2*i - 1) in
(omega

(i+1) dt dti knot
(union acc

[ W(xl(C(knot,ic)) ,
(if (over dt ic-1)

then yO(C (knot, ic-1) )
else yl(C(knot,ic-l)))) ;
W(yO(C(knot,ic)) ,
(if (over dt ic+1)

then xl(C (knot, ic+1) )
else xO(C(knot,ic+l)))) ;
W(xO(C(knot,ic)) ,
(if (over dt (dti ((dt ic)-l)))

then yO(C (knot, (dti ((dt ic)-l))))
else yl(C (knot, (dti ((dt ic)-l))))));
W(yl(C(knot,ic)) ,
(if (over dt (dti ((dt ic)+l)))

then xl(C (knot, (dti ((dt ic)+l))))

else xO(C (knot, (dti ((dt ic)+l)))))) ]))

else acc

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Acknowledgments. The authors wish to thank Matthias Radestock for sugges-
tions for coding wires, and early advocation of the wire-saturated form the final
encoding took and his probing questions regarding proof strategies in earlier drafts
of this paper. One of the co-author wishes to acknowledge his longstanding debt
to Samson Abramksy for making so accessible his foundational insights into the
Curry-Howard isomorphism. Additionally, the authors would like to thank the re-
viewers of ICALP 2006 for their helpful comments on an earlier write up of these
results.

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

References

[1] Martin Abadi and Bruno Blanchet. Analyzing security protocols with secrecy types

and logic programs. In POPL, pages 33-44, 2002.
[2] Martin Abadi and Bruno Blanchet. Secrecy types for asymmetric communication.

Theor. Comput. Set., 3(298):387-415, 2003.
[3] Samson Abramsky. Algorithmic game semantics and static analysis. In SAS, page 1,

2005.

[4] John C Baez. An introduction to spin foam models of quantum gravity and bf theory.

LECT.NOTES PHYS., 543:25, 2000.
[5] P. D. Bangert. Algorithmic Problems in the Braid Groups. PhD thesis, University

College London, 2002.

[6] Paul V. Biron and Ashok Malhotra. XML schema part 2: Datatypes second edition.

W3C recommendation, W3C, October 2004. http://www.w3.org/TR/2004/REC-

xmlschema-2-20041028 / .
[7] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating

sequential processes. J. Assoc. Comput. Mach., 31(3):560-599, 1984.
[8] Luis Caires. Behavioral and spatial observations in a logic for the pi-calculus. In

FoSSaCS, pages 72-89, 2004.
[9] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part i). Inf. Comput,

186(2) :194-235, 2003.

[10] Luis Caires and Luca Cardelli. A spatial logic for concurrency - ii. Theor. Comput.

Set., 322(3):517-565, 2004.
[11] Jorge A. Calvo, Kenneth C. Millett, Eric J. Rawdon, and Andrzej Stasiak, editors.

Physical and numerical models in knot theory, volume 36 of Series on Knots and

Everything. World Scientific Publishing Co. Pte. Ltd., Singapore, 2005. Including

applications to the life sciences.
[12] Jorge Alberto Calvo. Knot enumeration through flypes and twisted splices. J. Knot

Theory Ramifications, 6 (6): 785-798, 1997.
[13] Luca Cardelli. Brane calculi. In CMSB, pages 257-278, 2004.

[14] A. Caudron. Classification des noeuds et des enlacements. Prepublication Math.
d'Orsay, Orsay, France: Universite Paris-Sud, 1981.

[15] J. H. Conway. An enumeration of knots and links, and some of their algebraic prop-
erties. In J. Leech, editor, Computational Problems in Abstract Algebra (Proc. Conf,
Oxford, 1967), pages 329-358. Pergamon, Oxford, 1970.

[16] Vincent Danos and Cosimo Laneve. Core formal molecular biology. In ESOP, pages
302-318, 2003.

[17] C. H. Dowker and Morwen B. Thistlethwaite. Classification of knot projections.

Topology AppL, 16(1):19-31, 1983.
[18] David C. Fallside and Priscilla Walmsley. XML schema part 0: Primer second edition.

W3C recommendation, W3C, October 2004. http://www.w3.org/TR/2004/REC-

xmlschema-0-20041028 / .
[19] Wan Fokkink, Rob van Glabbeek, and Paulien de Wind. Compositionality of

Hennessy-Milner logic through structural operational semantics. In Fundamentals of

computation theory, volume 2751 of Lecture Notes in Comput. Set., pages 412-422.

Springer, Berlin, 2003.
[20] Cedric Fournet, Fabrice Le Fessant, Luc Maranget, and Alan Schmitt. Jocaml: A

language for concurrent distributed and mobile programming. In Advanced Functional

Programming, pages 129-158, 2002.
[21] Cedric Fournet, Georges Gontheir, Jean-Jacques Levy, Luc Maranget, and Didicr

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

Remy. A calculus of mobile agents. In Ugo Montanari and Vladimiro Sassone, editors,
CONCUR 1996, volume 1119 of Lecture Notes in Computer Science, pages 406-421.
Springer- Verlag, 1996.

[22] Rusins Freivalds. Knot theory, Jones polynomial and quantum computing. In Math-
ematical foundations of computer science 2005, volume 3618 of Lecture Notes in
Comput. Sci., pages 15-25. Springer, Berlin, 2005.

[23] C. A. R. Hoare. Communicating sequential processes. Prentice Hall International
Series in Computer Science. Prentice Hall International, Englewood Cliffs, NJ, 1985.
With a foreword by Edsger W. Dijkstra.

[24] C. A. R. Hoare. Notes on communicating sequential systems. In Control flow and
data flow: concepts of distributed programming (Marktoberdorf, 1984), volume 14 of
NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., pages 123-204. Springer, Berlin,
1985.

[25] C. A. R. Hoare. Algebraic specifications and proofs for communicating sequential
processes. In Logic of programming and calculi of discrete design (Marktoberdorf,
1986), volume 36 of NATO Adv. Sci. Inst. Ser. F Comput. Systems Set., pages 277-
300. Springer, Berlin, 1987.

[26] Jim Hoste. The enumeration and classification of knots and links. In Handbook of
knot theory, pages 209-232. Elsevier B. V., Amsterdam, 2005.

[27] Jim Hoste, Morwen Thistlethwaite, and Jeff Weeks. The first 1,701,936 knots. Math.
Intelligencer, 20(4):33-48, 1998.

[28] Allen L. Brown Jr., Cosimo Laneve, and L. Gregory Meredith. Piduce: A process
calculus with native xml datatypes. In Mario Bravetti, Leila Kloul, and Gianluigi
Zavattaro, editors, EPEW/WS-FM, volume 3670 of Lecture Notes in Computer Sci-
ence, pages 18-34. Springer, 2005.

[29] Louis Kauffman and Vassily Olegovich Manturov. Virtual knots and links, 2005.

[30] T. P. Kirkman. The enumeration, description, and construction of knots of fewer
than ten crossings. Trans. Roy. Soc. Edin., 32:281-309, 1885.

[31] Cosimo Laneve and Gianluigi Zavattaro. Foundations of web transactions. In FoS-
SaCS, pages 282-298, 2005.

[32] Tomas Liko and Louis H. Kauffman. Knot theory and a physical state of quantum
gravity. Classical Quantum Gravity, 23(4):R63-R90, 2006.

[33] J.B. Listing. Vorstudien zur topologie. Gottingen Studien, 2:811-875, 1848.

[34] C. N. Little. On knots, with a census to order 10. Trans. Conn. Acad. Sci., 18:374-
378, 1885.

[35] C. N. Little. Alternate ± knots of order 11. Trans. Roy. Soc. Edin., 36:253-255, 1890.

[36] C. N. Little. Non-alternate ± knots. Trans. Roy. Soc. Edin., 39:771-778, 1900.

[37] Charles Livingston. Knot Theory. Carus Mathematical Monographs. MAA, 1993.

[38] Noah Mendelsohn, Henry S. Thompson, David Beech, and Murray Maloney. XML
schema part 1: Structures second edition. W3C recommendation, W3C, October
2004. http://www.w3.org/TR/2004/REC-xmlschema-l-20041028/.

[39] Greg Meredith and Steve Bjorg. Contracts and types. Commun. ACM, 46(10):41-47,
2003.

[40] L. Gregory Meredith and Matthias Radestock. A reflective higher-order calculus.

Electr. Notes Theor. Comput. Sci., 141(5):49-67, 2005.
[41] L.G. Meredith and Matthias Radestock. A reflective higher-order calculus. In Mirko

Viroli, editor, ETAPS 2005 Satellites. Springer- Verlag, 2005.
[42] R. Milner and D. Sangiorgi. Techniques of weak bisimulation up-to, 1992.
[43] Robin Milner. A Calculus of Communicating Systems. Springer Verlag, 1980.
[44] Robin Milner. Elements of interaction - turing award lecture. Commun. ACM,

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir

36(l):78-89, 1993.

[45] Robin Milner. The polyadic 7r-calculus: A tutorial. Logic and Algebra of Specification,
Springer- Verlag, 1993.

[46] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes. I,

II. Inform, and Comput., 100(l):l-40, 41-77, 1992.
[47] Robin Milner and Davide Sangiorgi. Barbed bisimulation. In ICALP, pages 685-695,

1992.

[48] Damien Pous. Weak bisimulation up to elaboration. In Christel Baier and Holger

Hermanns, editors, CONCUR, volume 4137 of Lecture Notes in Computer Science,

pages 390-405. Springer, 2006.
[49] Corrado Priami, Aviv Regev, Ehud Y. Shapiro, and William Silverman. Application

of a stochastic name-passing calculus to representation and simulation of molecular

processes. Inf. Process. Lett., 80(1):25-31, 2001.
[50] Stuart Rankin and Ortho Flint. Enumerating the prime alternating links. J. Knot

Theory Ramifications, 13(1):151-173, 2004.
[51] Stuart Rankin, Ortho Flint, and John Schermann. Enumerating the prime alternating

knots. I. J. Knot Theory Ramifications, 13(1):57-100, 2004.
[52] Stuart Rankin, Ortho Flint, and John Schermann. Enumerating the prime alternating

knots. II. J. Knot Theory Ramifications, 13(1):101-149, 2004.
[53] R. C. Read and P. Rosenstiehl. On the gauss crossing problem. Proc. Fifth Hungarian

Comb. Colloq., 1977.

[54] Amitai Regev and Ehud Y. Shapiro. Cells as computation. In CMSB, pages 1-3,
2003.

[55] Kurt Reidemeister. Knoten und Verkettungen. Math. Z., 29(l):713-729, 1929.

[56] David Sangiorgi and David Walker. The -K-Calculus: A Theory of Mobile Processes.

Cambridge University Press, 2001.
[57] Davide Sangiorgi. On the proof method for bisimulation (extended abstract). In

MFCS, pages 479-488, 1995.
[58] Davide Sangiorgi. Bisimulation in higher-order process calculi. Information and Com-
putation, 131:141-178, 1996.
[59] Davide Sangiorgi. Bisimulation: From the origins to today. In LICS, pages 298-302.

IEEE Computer Society, 2004.
[60] Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to" . In

CONCUR, pages 32-46, 1992.
[61] Robert G. Scharein. Interactive Topological Drawing. PhD thesis, Department of

Computer Science, The University of British Columbia, 1998.
[62] Jerome Simeon, Denise Draper, Ashok Malhotra, Peter Fankhauser, Mary

Fernandez, Michael Rys, Philip Wadler, and Kristoffer Rose. XQuery 1.0 and

XPath 2.0 formal semantics. Candidate recommendation, W3C, June 2006.

http://www.w3.org/TR/2006/CR-xquery-semantics-20060608/.
[63] P.G. Tait. On knots, i, ii, iii. In Scientific Papers, volume 1, pages 273-347. Cambridge

University Press, Cambridge, 1898.
[64] Pawel T. Wojciechowski and Peter Sewell. Nomadic pict: Language and infrastructure

design for mobile agents. In ASA/MA, pages 2-12, 1999.